i, x:Id, k:Knd, ds:x:Id fp Type, T:Type, f:(State(ds)TDeclaredType(ds;x)).
Normal(ds)
 Normal(T)
 (isrcv(k)  i = destination(lnk(k)))
 @i effect k(v:T)  x := f State(ds) v 
 ||- es.@i events of kind k change x to f State(ds) (val:T) 

latex

Definitions	es realizer ind Reffect compseq tag def, Consistent(R;es), ES, t  T, P  Q, x:A. B(x), @loc effect knd(v:T)  x := f State(ds) v , @i events of kind k change x to f State(ds) (val:T), x:AB(x), A & B, P & Q, b, R-Feasible(R), inr(x), x:AB(x), R ||- es.P(es), Id, Knd, Type, x. t(x), a:A fp B(a), DeclaredType(ds;x), State(ds), Normal(ds), Normal(T), lnk(k), destination(l), s = t, Prop, isrcv(k)
Lemmas	assert wf, isrcv wf, ldst wf, lnk wf, normal-type wf, normal-ds wf, decl-state wf, decl-type wf, fpf wf, Knd wf, Id wf, R-consistent wf, Reffect wf, event system wf